a,b:. (a = b)  ((a = b)) 

latex

Definitions	x:A. B(x), , P  Q, P  Q, prop{i:l}, P  Q, t  T, x. t(x), P  Q, T, True, x(s), A  B, A, False
Lemmas	all functionality wrt iff, nat wf, iff wf, assert wf, eq int wf, iff functionality wrt iff, assert of eq int, le wf